A, B:Type, f:(A(B + Top)). p-id() o f   = f 

latex

ProofTree

Definitions	t  T, Type, x:AB(x), b, False, A, s = t, p-id(), f(a), Top, left + right, if b then t else f fi , P  Q, x:A. B(x), , x:A  B(x), P & Q, P  Q, Unit, x.A(x), f o g  , True, do-apply(f;x), can-apply(f;x)
Lemmas	true wf, false wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot